(declare-fun a () Int)
(declare-fun b () Int)
(assert (<= 0 a))
(declare-fun c (Int) Bool)
(declare-fun ab (Int) Int)
(declare-fun j (Int) Bool)
(declare-fun ac (Int) Int)
(push)
(assert (= (= 0 1) (j 0)))
(assert (= (ac 0) (ite (= b 0) (ab 0) 0)))
(assert (not (j 0)))
(assert (let ((az (not (c 0)))) (and az az)))
(check-sat)
